(0) Obligation:
Clauses:
tautology(F) :- reduce(sequent([], .(F, [])), sequent([], [])).
reduce(sequent(.(if(A, B), Fs), Gs), NF) :- reduce(sequent(.(+(-(B), A), Fs), Gs), NF).
reduce(sequent(.(iff(A, B), Fs), Gs), NF) :- reduce(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF).
reduce(sequent(.(*(F1, F2), Fs), Gs), NF) :- reduce(sequent(.(F1, .(F2, Fs)), Gs), NF).
reduce(sequent(.(+(F1, F2), Fs), Gs), NF) :- ','(reduce(sequent(.(F1, Fs), Gs), NF), reduce(sequent(.(F2, Fs), Gs), NF)).
reduce(sequent(.(-(F1), Fs), Gs), NF) :- reduce(sequent(Fs, .(F1, Gs)), NF).
reduce(sequent(Fs, .(if(A, B), Gs)), NF) :- reduce(sequent(Fs, .(+(-(B), A), Gs)), NF).
reduce(sequent(Fs, .(iff(A, B), Gs)), NF) :- reduce(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF).
reduce(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) :- reduce(sequent(Fs, Gs), sequent(.(p(V), Left), Right)).
reduce(sequent(Fs, .(+(G1, G2), Gs)), NF) :- reduce(sequent(Fs, .(G1, .(G2, Gs))), NF).
reduce(sequent(Fs, .(*(G1, G2), Gs)), NF) :- ','(reduce(sequent(Fs, .(G1, Gs)), NF), reduce(sequent(Fs, .(G2, Gs)), NF)).
reduce(sequent(Fs, .(-(G1), Gs)), NF) :- reduce(sequent(.(G1, Fs), Gs), NF).
reduce(sequent([], .(p(V), Gs)), sequent(Left, Right)) :- reduce(sequent([], Gs), sequent(Left, .(p(V), Right))).
reduce(sequent([], []), sequent(F1, F2)) :- intersect(F1, F2).
intersect(.(X, X1), .(X, X2)).
intersect(Xs, .(X3, Ys)) :- intersect(Xs, Ys).
intersect(.(X4, Xs), Ys) :- intersect(Xs, Ys).
yes1 :- tautology(+(-(p(1)), p(1))).
yes2 :- tautology(*(+(-(p(1)), p(1)), +(p(1), -(p(1))))).
yes3 :- tautology(*(+(-(-(-(p(1)))), p(1)), +(-(-(p(1))), -(p(1))))).
yes4 :- tautology(-(-(','(p(1), *), p(1)))).
no1 :- tautology(-(','(p(1), *), p(1))).
no2 :- tautology(+(-(+(p(1), -(p(1)))), p(2))).
no3 :- tautology(*(+(-(+(-(p(1)), +(-(p(2)), p(3)))), +(-(+(p(1), p(2))), p(3))), +(-(p(1)), +(+(-(p(2)), p(3)), -(+(-(+(p(1), p(2))), p(3))))))).
no4 :- tautology(+(-(+(*(p(1), *(p(2), p(3))), -(','(-(p(1)), *), -(','(p(2), *), p(3))))), *(+(-(p(1)), *(+(-(p(2)), p(3)), +(p(2), -(p(3))))), +(p(1), -(*(+(-(p(2)), p(3)), +(p(2), -(p(3))))))))).
Query: tautology(g)
(1) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
tautology_in: (b)
reduce_in: (b,b)
intersect_in: (b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
tautology_in_g(F) → U1_g(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U1_g(F, reduce_out_gg(sequent([], .(F, [])), sequent([], []))) → tautology_out_g(F)
The argument filtering Pi contains the following mapping:
tautology_in_g(
x1) =
tautology_in_g(
x1)
U1_g(
x1,
x2) =
U1_g(
x2)
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
tautology_out_g(
x1) =
tautology_out_g
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
tautology_in_g(F) → U1_g(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U1_g(F, reduce_out_gg(sequent([], .(F, [])), sequent([], []))) → tautology_out_g(F)
The argument filtering Pi contains the following mapping:
tautology_in_g(
x1) =
tautology_in_g(
x1)
U1_g(
x1,
x2) =
U1_g(
x2)
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
tautology_out_g(
x1) =
tautology_out_g
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
TAUTOLOGY_IN_G(F) → U1_G(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
TAUTOLOGY_IN_G(F) → REDUCE_IN_GG(sequent([], .(F, [])), sequent([], []))
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → U2_GG(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → U3_GG(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → U7_GG(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → U8_GG(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_GG(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_GG(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → U14_GG(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_GG(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
REDUCE_IN_GG(sequent([], []), sequent(F1, F2)) → U16_GG(F1, F2, intersect_in_gg(F1, F2))
REDUCE_IN_GG(sequent([], []), sequent(F1, F2)) → INTERSECT_IN_GG(F1, F2)
INTERSECT_IN_GG(Xs, .(X3, Ys)) → U17_GG(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
INTERSECT_IN_GG(Xs, .(X3, Ys)) → INTERSECT_IN_GG(Xs, Ys)
INTERSECT_IN_GG(.(X4, Xs), Ys) → U18_GG(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
INTERSECT_IN_GG(.(X4, Xs), Ys) → INTERSECT_IN_GG(Xs, Ys)
U12_GG(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U12_GG(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
U5_GG(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U5_GG(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
The TRS R consists of the following rules:
tautology_in_g(F) → U1_g(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U1_g(F, reduce_out_gg(sequent([], .(F, [])), sequent([], []))) → tautology_out_g(F)
The argument filtering Pi contains the following mapping:
tautology_in_g(
x1) =
tautology_in_g(
x1)
U1_g(
x1,
x2) =
U1_g(
x2)
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
tautology_out_g(
x1) =
tautology_out_g
TAUTOLOGY_IN_G(
x1) =
TAUTOLOGY_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x2)
REDUCE_IN_GG(
x1,
x2) =
REDUCE_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_GG(
x6)
U3_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_GG(
x6)
U4_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GG(
x6)
U5_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GG(
x2,
x3,
x4,
x5,
x6)
U7_GG(
x1,
x2,
x3,
x4,
x5) =
U7_GG(
x5)
U8_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_GG(
x6)
U9_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_GG(
x6)
U10_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_GG(
x6)
U11_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_GG(
x6)
U12_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_GG(
x1,
x3,
x4,
x5,
x6)
U14_GG(
x1,
x2,
x3,
x4,
x5) =
U14_GG(
x5)
U15_GG(
x1,
x2,
x3,
x4,
x5) =
U15_GG(
x5)
U16_GG(
x1,
x2,
x3) =
U16_GG(
x3)
INTERSECT_IN_GG(
x1,
x2) =
INTERSECT_IN_GG(
x1,
x2)
U17_GG(
x1,
x2,
x3,
x4) =
U17_GG(
x4)
U18_GG(
x1,
x2,
x3,
x4) =
U18_GG(
x4)
U13_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_GG(
x6)
U6_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_GG(
x6)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
TAUTOLOGY_IN_G(F) → U1_G(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
TAUTOLOGY_IN_G(F) → REDUCE_IN_GG(sequent([], .(F, [])), sequent([], []))
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → U2_GG(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → U3_GG(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → U7_GG(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → U8_GG(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_GG(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_GG(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → U14_GG(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_GG(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
REDUCE_IN_GG(sequent([], []), sequent(F1, F2)) → U16_GG(F1, F2, intersect_in_gg(F1, F2))
REDUCE_IN_GG(sequent([], []), sequent(F1, F2)) → INTERSECT_IN_GG(F1, F2)
INTERSECT_IN_GG(Xs, .(X3, Ys)) → U17_GG(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
INTERSECT_IN_GG(Xs, .(X3, Ys)) → INTERSECT_IN_GG(Xs, Ys)
INTERSECT_IN_GG(.(X4, Xs), Ys) → U18_GG(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
INTERSECT_IN_GG(.(X4, Xs), Ys) → INTERSECT_IN_GG(Xs, Ys)
U12_GG(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U12_GG(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
U5_GG(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U5_GG(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
The TRS R consists of the following rules:
tautology_in_g(F) → U1_g(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U1_g(F, reduce_out_gg(sequent([], .(F, [])), sequent([], []))) → tautology_out_g(F)
The argument filtering Pi contains the following mapping:
tautology_in_g(
x1) =
tautology_in_g(
x1)
U1_g(
x1,
x2) =
U1_g(
x2)
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
tautology_out_g(
x1) =
tautology_out_g
TAUTOLOGY_IN_G(
x1) =
TAUTOLOGY_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x2)
REDUCE_IN_GG(
x1,
x2) =
REDUCE_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_GG(
x6)
U3_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_GG(
x6)
U4_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GG(
x6)
U5_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GG(
x2,
x3,
x4,
x5,
x6)
U7_GG(
x1,
x2,
x3,
x4,
x5) =
U7_GG(
x5)
U8_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_GG(
x6)
U9_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_GG(
x6)
U10_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_GG(
x6)
U11_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_GG(
x6)
U12_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_GG(
x1,
x3,
x4,
x5,
x6)
U14_GG(
x1,
x2,
x3,
x4,
x5) =
U14_GG(
x5)
U15_GG(
x1,
x2,
x3,
x4,
x5) =
U15_GG(
x5)
U16_GG(
x1,
x2,
x3) =
U16_GG(
x3)
INTERSECT_IN_GG(
x1,
x2) =
INTERSECT_IN_GG(
x1,
x2)
U17_GG(
x1,
x2,
x3,
x4) =
U17_GG(
x4)
U18_GG(
x1,
x2,
x3,
x4) =
U18_GG(
x4)
U13_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_GG(
x6)
U6_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_GG(
x6)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 18 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
INTERSECT_IN_GG(.(X4, Xs), Ys) → INTERSECT_IN_GG(Xs, Ys)
INTERSECT_IN_GG(Xs, .(X3, Ys)) → INTERSECT_IN_GG(Xs, Ys)
The TRS R consists of the following rules:
tautology_in_g(F) → U1_g(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U1_g(F, reduce_out_gg(sequent([], .(F, [])), sequent([], []))) → tautology_out_g(F)
The argument filtering Pi contains the following mapping:
tautology_in_g(
x1) =
tautology_in_g(
x1)
U1_g(
x1,
x2) =
U1_g(
x2)
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
tautology_out_g(
x1) =
tautology_out_g
INTERSECT_IN_GG(
x1,
x2) =
INTERSECT_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
INTERSECT_IN_GG(.(X4, Xs), Ys) → INTERSECT_IN_GG(Xs, Ys)
INTERSECT_IN_GG(Xs, .(X3, Ys)) → INTERSECT_IN_GG(Xs, Ys)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INTERSECT_IN_GG(.(X4, Xs), Ys) → INTERSECT_IN_GG(Xs, Ys)
INTERSECT_IN_GG(Xs, .(X3, Ys)) → INTERSECT_IN_GG(Xs, Ys)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- INTERSECT_IN_GG(.(X4, Xs), Ys) → INTERSECT_IN_GG(Xs, Ys)
The graph contains the following edges 1 > 1, 2 >= 2
- INTERSECT_IN_GG(Xs, .(X3, Ys)) → INTERSECT_IN_GG(Xs, Ys)
The graph contains the following edges 1 >= 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
U12_GG(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The TRS R consists of the following rules:
tautology_in_g(F) → U1_g(F, reduce_in_gg(sequent([], .(F, [])), sequent([], [])))
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U1_g(F, reduce_out_gg(sequent([], .(F, [])), sequent([], []))) → tautology_out_g(F)
The argument filtering Pi contains the following mapping:
tautology_in_g(
x1) =
tautology_in_g(
x1)
U1_g(
x1,
x2) =
U1_g(
x2)
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
tautology_out_g(
x1) =
tautology_out_g
REDUCE_IN_GG(
x1,
x2) =
REDUCE_IN_GG(
x1,
x2)
U5_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GG(
x2,
x3,
x4,
x5,
x6)
U12_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_GG(
x1,
x3,
x4,
x5,
x6)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
U12_GG(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(A, B, Fs, Gs, NF, reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(F1, Fs, Gs, NF, reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(Fs, A, B, Gs, NF, reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(V, Fs, Gs, Left, Right, reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(Fs, G1, Gs, NF, reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(V, Gs, Left, Right, reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(+(-(B), A), Fs), Gs), NF)) → reduce_out_gg(sequent(.(if(A, B), Fs), Gs), NF)
U3_gg(A, B, Fs, Gs, NF, reduce_out_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)) → reduce_out_gg(sequent(.(iff(A, B), Fs), Gs), NF)
U4_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, .(F2, Fs)), Gs), NF)) → reduce_out_gg(sequent(.(*(F1, F2), Fs), Gs), NF)
U5_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F1, Fs), Gs), NF)) → U6_gg(F1, F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(F1, Fs, Gs, NF, reduce_out_gg(sequent(Fs, .(F1, Gs)), NF)) → reduce_out_gg(sequent(.(-(F1), Fs), Gs), NF)
U8_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(+(-(B), A), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(if(A, B), Gs)), NF)
U9_gg(Fs, A, B, Gs, NF, reduce_out_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)) → reduce_out_gg(sequent(Fs, .(iff(A, B), Gs)), NF)
U10_gg(V, Fs, Gs, Left, Right, reduce_out_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right))) → reduce_out_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right))
U11_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, .(G2, Gs))), NF)) → reduce_out_gg(sequent(Fs, .(+(G1, G2), Gs)), NF)
U12_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G1, Gs)), NF)) → U13_gg(Fs, G1, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(Fs, G1, Gs, NF, reduce_out_gg(sequent(.(G1, Fs), Gs), NF)) → reduce_out_gg(sequent(Fs, .(-(G1), Gs)), NF)
U15_gg(V, Gs, Left, Right, reduce_out_gg(sequent([], Gs), sequent(Left, .(p(V), Right)))) → reduce_out_gg(sequent([], .(p(V), Gs)), sequent(Left, Right))
U6_gg(F1, F2, Fs, Gs, NF, reduce_out_gg(sequent(.(F2, Fs), Gs), NF)) → reduce_out_gg(sequent(.(+(F1, F2), Fs), Gs), NF)
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(F1, F2, intersect_in_gg(F1, F2))
U13_gg(Fs, G1, G2, Gs, NF, reduce_out_gg(sequent(Fs, .(G2, Gs)), NF)) → reduce_out_gg(sequent(Fs, .(*(G1, G2), Gs)), NF)
U16_gg(F1, F2, intersect_out_gg(F1, F2)) → reduce_out_gg(sequent([], []), sequent(F1, F2))
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg(.(X, X1), .(X, X2))
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(Xs, X3, Ys, intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(X4, Xs, Ys, intersect_in_gg(Xs, Ys))
U17_gg(Xs, X3, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(Xs, .(X3, Ys))
U18_gg(X4, Xs, Ys, intersect_out_gg(Xs, Ys)) → intersect_out_gg(.(X4, Xs), Ys)
The argument filtering Pi contains the following mapping:
reduce_in_gg(
x1,
x2) =
reduce_in_gg(
x1,
x2)
sequent(
x1,
x2) =
sequent(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
if(
x1,
x2) =
if(
x1,
x2)
U2_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_gg(
x6)
iff(
x1,
x2) =
iff(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U3_gg(
x6)
*(
x1,
x2) =
*(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gg(
x6)
+(
x1,
x2) =
+(
x1,
x2)
U5_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gg(
x2,
x3,
x4,
x5,
x6)
-(
x1) =
-(
x1)
U7_gg(
x1,
x2,
x3,
x4,
x5) =
U7_gg(
x5)
U8_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U8_gg(
x6)
U9_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U9_gg(
x6)
p(
x1) =
p(
x1)
U10_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U10_gg(
x6)
U11_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gg(
x6)
U12_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_gg(
x1,
x3,
x4,
x5,
x6)
U14_gg(
x1,
x2,
x3,
x4,
x5) =
U14_gg(
x5)
[] =
[]
U15_gg(
x1,
x2,
x3,
x4,
x5) =
U15_gg(
x5)
U16_gg(
x1,
x2,
x3) =
U16_gg(
x3)
intersect_in_gg(
x1,
x2) =
intersect_in_gg(
x1,
x2)
intersect_out_gg(
x1,
x2) =
intersect_out_gg
U17_gg(
x1,
x2,
x3,
x4) =
U17_gg(
x4)
U18_gg(
x1,
x2,
x3,
x4) =
U18_gg(
x4)
reduce_out_gg(
x1,
x2) =
reduce_out_gg
U13_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_gg(
x6)
U6_gg(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gg(
x6)
REDUCE_IN_GG(
x1,
x2) =
REDUCE_IN_GG(
x1,
x2)
U5_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GG(
x2,
x3,
x4,
x5,
x6)
U12_GG(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_GG(
x1,
x3,
x4,
x5,
x6)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
U12_GG(Fs, G2, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(19) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
REDUCE_IN_GG(sequent(Fs, .(iff(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
| POL(REDUCE_IN_GG(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
| POL(sequent(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(if(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(+(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(U5_GG(x1, x2, x3, x4, x5)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 | + | | · | x5 |
| POL(reduce_in_gg(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(iff(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(*(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(U12_GG(x1, x2, x3, x4, x5)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 | + | | · | x5 |
| POL(U5_gg(x1, x2, x3, x4, x5)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 | + | | · | x5 |
| POL(U12_gg(x1, x2, x3, x4, x5)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 | + | | · | x5 |
| POL(intersect_in_gg(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
U12_GG(Fs, G2, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(21) QDPQMonotonicMRRProof (EQUIVALENT transformation)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented dependency pairs:
REDUCE_IN_GG(sequent(.(*(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, .(F2, Fs)), Gs), NF)
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_GG(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
REDUCE_IN_GG(sequent(Fs, .(*(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, Gs)), NF)
Used ordering: Polynomial interpretation [POLO]:
POL(*(x1, x2)) = 1 + x1 + x2
POL(+(x1, x2)) = x1 + x2
POL(-(x1)) = x1
POL(.(x1, x2)) = 2·x1 + x2
POL(REDUCE_IN_GG(x1, x2)) = x1
POL(U10_gg(x1)) = 0
POL(U11_gg(x1)) = 0
POL(U12_GG(x1, x2, x3, x4, x5)) = x1 + 2·x2 + x3
POL(U12_gg(x1, x2, x3, x4, x5)) = 0
POL(U13_gg(x1)) = 0
POL(U14_gg(x1)) = 0
POL(U15_gg(x1)) = 0
POL(U16_gg(x1)) = 0
POL(U17_gg(x1)) = 0
POL(U18_gg(x1)) = 0
POL(U2_gg(x1)) = 0
POL(U3_gg(x1)) = 0
POL(U4_gg(x1)) = 0
POL(U5_GG(x1, x2, x3, x4, x5)) = 2·x1 + x2 + x3
POL(U5_gg(x1, x2, x3, x4, x5)) = 0
POL(U6_gg(x1)) = 0
POL(U7_gg(x1)) = 0
POL(U8_gg(x1)) = 0
POL(U9_gg(x1)) = 0
POL([]) = 0
POL(if(x1, x2)) = x1 + x2
POL(iff(x1, x2)) = 1 + 2·x1 + 2·x2
POL(intersect_in_gg(x1, x2)) = 0
POL(intersect_out_gg) = 0
POL(p(x1)) = 0
POL(reduce_in_gg(x1, x2)) = 0
POL(reduce_out_gg) = 0
POL(sequent(x1, x2)) = x1 + x2
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
U12_GG(Fs, G2, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(Fs, .(G2, Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(25) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
REDUCE_IN_GG(sequent(.(iff(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(-(F1), Fs), Gs), NF) → REDUCE_IN_GG(sequent(Fs, .(F1, Gs)), NF)
REDUCE_IN_GG(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE_IN_GG(sequent(Fs, Gs), sequent(.(p(V), Left), Right))
REDUCE_IN_GG(sequent(Fs, .(-(G1), Gs)), NF) → REDUCE_IN_GG(sequent(.(G1, Fs), Gs), NF)
REDUCE_IN_GG(sequent([], .(p(V), Gs)), sequent(Left, Right)) → REDUCE_IN_GG(sequent([], Gs), sequent(Left, .(p(V), Right)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(*(x1, x2)) = 0
POL(+(x1, x2)) = x1 + x2
POL(-(x1)) = 1 + x1
POL(.(x1, x2)) = x1 + x2
POL(REDUCE_IN_GG(x1, x2)) = x1
POL(U10_gg(x1)) = 0
POL(U11_gg(x1)) = 0
POL(U12_gg(x1, x2, x3, x4, x5)) = 0
POL(U13_gg(x1)) = 0
POL(U14_gg(x1)) = 0
POL(U15_gg(x1)) = 0
POL(U16_gg(x1)) = 0
POL(U17_gg(x1)) = 0
POL(U18_gg(x1)) = 1
POL(U2_gg(x1)) = 0
POL(U3_gg(x1)) = 0
POL(U4_gg(x1)) = 0
POL(U5_GG(x1, x2, x3, x4, x5)) = x1 + x2 + x3
POL(U5_gg(x1, x2, x3, x4, x5)) = 0
POL(U6_gg(x1)) = 0
POL(U7_gg(x1)) = 0
POL(U8_gg(x1)) = 0
POL(U9_gg(x1)) = 0
POL([]) = 0
POL(if(x1, x2)) = 1 + x1 + x2
POL(iff(x1, x2)) = 1 + x1 + x2
POL(intersect_in_gg(x1, x2)) = 1 + x1
POL(intersect_out_gg) = 0
POL(p(x1)) = 1
POL(reduce_in_gg(x1, x2)) = 0
POL(reduce_out_gg) = 0
POL(sequent(x1, x2)) = x1 + x2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(27) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
REDUCE_IN_GG(sequent(Fs, .(+(G1, G2), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(G1, .(G2, Gs))), NF)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(*(x1, x2)) = 0
POL(+(x1, x2)) = 1 + x1
POL(-(x1)) = 0
POL(.(x1, x2)) = x1
POL(REDUCE_IN_GG(x1, x2)) = x1
POL(U10_gg(x1)) = 0
POL(U11_gg(x1)) = 0
POL(U12_gg(x1, x2, x3, x4, x5)) = 0
POL(U13_gg(x1)) = 0
POL(U14_gg(x1)) = 0
POL(U15_gg(x1)) = 0
POL(U16_gg(x1)) = 0
POL(U17_gg(x1)) = 0
POL(U18_gg(x1)) = 0
POL(U2_gg(x1)) = 0
POL(U3_gg(x1)) = 0
POL(U4_gg(x1)) = 0
POL(U5_GG(x1, x2, x3, x4, x5)) = x3
POL(U5_gg(x1, x2, x3, x4, x5)) = 0
POL(U6_gg(x1)) = 0
POL(U7_gg(x1)) = 0
POL(U8_gg(x1)) = 0
POL(U9_gg(x1)) = 0
POL([]) = 0
POL(if(x1, x2)) = 1 + x2
POL(iff(x1, x2)) = 0
POL(intersect_in_gg(x1, x2)) = 0
POL(intersect_out_gg) = 0
POL(p(x1)) = 0
POL(reduce_in_gg(x1, x2)) = 0
POL(reduce_out_gg) = 0
POL(sequent(x1, x2)) = x2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(29) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
REDUCE_IN_GG(sequent(Fs, .(if(A, B), Gs)), NF) → REDUCE_IN_GG(sequent(Fs, .(+(-(B), A), Gs)), NF)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(*(x1, x2)) = 0
POL(+(x1, x2)) = 0
POL(-(x1)) = 0
POL(.(x1, x2)) = x1
POL(REDUCE_IN_GG(x1, x2)) = x1
POL(U10_gg(x1)) = 0
POL(U11_gg(x1)) = 0
POL(U12_gg(x1, x2, x3, x4, x5)) = 0
POL(U13_gg(x1)) = 0
POL(U14_gg(x1)) = 0
POL(U15_gg(x1)) = 0
POL(U16_gg(x1)) = 0
POL(U17_gg(x1)) = 0
POL(U18_gg(x1)) = 0
POL(U2_gg(x1)) = 0
POL(U3_gg(x1)) = 0
POL(U4_gg(x1)) = 0
POL(U5_GG(x1, x2, x3, x4, x5)) = x3
POL(U5_gg(x1, x2, x3, x4, x5)) = 0
POL(U6_gg(x1)) = 0
POL(U7_gg(x1)) = 0
POL(U8_gg(x1)) = 0
POL(U9_gg(x1)) = 0
POL([]) = 0
POL(if(x1, x2)) = 1
POL(iff(x1, x2)) = 0
POL(intersect_in_gg(x1, x2)) = 0
POL(intersect_out_gg) = 0
POL(p(x1)) = 0
POL(reduce_in_gg(x1, x2)) = 0
POL(reduce_out_gg) = 0
POL(sequent(x1, x2)) = x2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(31) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_GG(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
REDUCE_IN_GG(sequent(.(+(F1, F2), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(F1, Fs), Gs), NF)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(*(x1, x2)) = 0
POL(+(x1, x2)) = 1 + x1 + x2
POL(-(x1)) = 0
POL(.(x1, x2)) = x1 + x2
POL(REDUCE_IN_GG(x1, x2)) = x1 + x2
POL(U10_gg(x1)) = 0
POL(U11_gg(x1)) = 0
POL(U12_gg(x1, x2, x3, x4, x5)) = 0
POL(U13_gg(x1)) = 0
POL(U14_gg(x1)) = 0
POL(U15_gg(x1)) = 0
POL(U16_gg(x1)) = 1
POL(U17_gg(x1)) = 0
POL(U18_gg(x1)) = 0
POL(U2_gg(x1)) = 0
POL(U3_gg(x1)) = 0
POL(U4_gg(x1)) = 0
POL(U5_GG(x1, x2, x3, x4, x5)) = x1 + x2 + x3 + x4
POL(U5_gg(x1, x2, x3, x4, x5)) = 0
POL(U6_gg(x1)) = 0
POL(U7_gg(x1)) = 0
POL(U8_gg(x1)) = 0
POL(U9_gg(x1)) = 0
POL([]) = 0
POL(if(x1, x2)) = 1 + x1 + x2
POL(iff(x1, x2)) = 0
POL(intersect_in_gg(x1, x2)) = 1 + x1 + x2
POL(intersect_out_gg) = 0
POL(p(x1)) = 0
POL(reduce_in_gg(x1, x2)) = 1 + x2
POL(reduce_out_gg) = 0
POL(sequent(x1, x2)) = x1 + x2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U5_GG(F2, Fs, Gs, NF, reduce_out_gg) → REDUCE_IN_GG(sequent(.(F2, Fs), Gs), NF)
REDUCE_IN_GG(sequent(.(if(A, B), Fs), Gs), NF) → REDUCE_IN_GG(sequent(.(+(-(B), A), Fs), Gs), NF)
The TRS R consists of the following rules:
reduce_in_gg(sequent(.(if(A, B), Fs), Gs), NF) → U2_gg(reduce_in_gg(sequent(.(+(-(B), A), Fs), Gs), NF))
reduce_in_gg(sequent(.(iff(A, B), Fs), Gs), NF) → U3_gg(reduce_in_gg(sequent(.(*(if(A, B), if(B, A)), Fs), Gs), NF))
reduce_in_gg(sequent(.(*(F1, F2), Fs), Gs), NF) → U4_gg(reduce_in_gg(sequent(.(F1, .(F2, Fs)), Gs), NF))
reduce_in_gg(sequent(.(+(F1, F2), Fs), Gs), NF) → U5_gg(F2, Fs, Gs, NF, reduce_in_gg(sequent(.(F1, Fs), Gs), NF))
reduce_in_gg(sequent(.(-(F1), Fs), Gs), NF) → U7_gg(reduce_in_gg(sequent(Fs, .(F1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(if(A, B), Gs)), NF) → U8_gg(reduce_in_gg(sequent(Fs, .(+(-(B), A), Gs)), NF))
reduce_in_gg(sequent(Fs, .(iff(A, B), Gs)), NF) → U9_gg(reduce_in_gg(sequent(Fs, .(*(if(A, B), if(B, A)), Gs)), NF))
reduce_in_gg(sequent(.(p(V), Fs), Gs), sequent(Left, Right)) → U10_gg(reduce_in_gg(sequent(Fs, Gs), sequent(.(p(V), Left), Right)))
reduce_in_gg(sequent(Fs, .(+(G1, G2), Gs)), NF) → U11_gg(reduce_in_gg(sequent(Fs, .(G1, .(G2, Gs))), NF))
reduce_in_gg(sequent(Fs, .(*(G1, G2), Gs)), NF) → U12_gg(Fs, G2, Gs, NF, reduce_in_gg(sequent(Fs, .(G1, Gs)), NF))
reduce_in_gg(sequent(Fs, .(-(G1), Gs)), NF) → U14_gg(reduce_in_gg(sequent(.(G1, Fs), Gs), NF))
reduce_in_gg(sequent([], .(p(V), Gs)), sequent(Left, Right)) → U15_gg(reduce_in_gg(sequent([], Gs), sequent(Left, .(p(V), Right))))
U2_gg(reduce_out_gg) → reduce_out_gg
U3_gg(reduce_out_gg) → reduce_out_gg
U4_gg(reduce_out_gg) → reduce_out_gg
U5_gg(F2, Fs, Gs, NF, reduce_out_gg) → U6_gg(reduce_in_gg(sequent(.(F2, Fs), Gs), NF))
U7_gg(reduce_out_gg) → reduce_out_gg
U8_gg(reduce_out_gg) → reduce_out_gg
U9_gg(reduce_out_gg) → reduce_out_gg
U10_gg(reduce_out_gg) → reduce_out_gg
U11_gg(reduce_out_gg) → reduce_out_gg
U12_gg(Fs, G2, Gs, NF, reduce_out_gg) → U13_gg(reduce_in_gg(sequent(Fs, .(G2, Gs)), NF))
U14_gg(reduce_out_gg) → reduce_out_gg
U15_gg(reduce_out_gg) → reduce_out_gg
U6_gg(reduce_out_gg) → reduce_out_gg
reduce_in_gg(sequent([], []), sequent(F1, F2)) → U16_gg(intersect_in_gg(F1, F2))
U13_gg(reduce_out_gg) → reduce_out_gg
U16_gg(intersect_out_gg) → reduce_out_gg
intersect_in_gg(.(X, X1), .(X, X2)) → intersect_out_gg
intersect_in_gg(Xs, .(X3, Ys)) → U17_gg(intersect_in_gg(Xs, Ys))
intersect_in_gg(.(X4, Xs), Ys) → U18_gg(intersect_in_gg(Xs, Ys))
U17_gg(intersect_out_gg) → intersect_out_gg
U18_gg(intersect_out_gg) → intersect_out_gg
The set Q consists of the following terms:
reduce_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
U4_gg(x0)
U5_gg(x0, x1, x2, x3, x4)
U7_gg(x0)
U8_gg(x0)
U9_gg(x0)
U10_gg(x0)
U11_gg(x0)
U12_gg(x0, x1, x2, x3, x4)
U14_gg(x0)
U15_gg(x0)
U6_gg(x0)
U13_gg(x0)
U16_gg(x0)
intersect_in_gg(x0, x1)
U17_gg(x0)
U18_gg(x0)
We have to consider all (P,Q,R)-chains.
(33) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(34) TRUE